Step of Proof: choicef_lemma
12,41
postcript
pdf
Inference at
*
I
of proof for Lemma
choicef
lemma
:
%xm
:XM,
T
:Type,
P
:(
T
). (
a
:
T
.
P
(
a
))
P
(
x
:
T
.
P
(
x
))
latex
by Fiat
latex
.
origin
%xm:XM, T:Type, P:(T
). (
a:T. P(a)) 
P(
x:T. P(x))
by Fiat
. %xm:XM, T:Type, P:(T). (a:T. P(a)) P(x:T. P(x))
by Fiat
.